DIRS := src driver

COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(d))

COQCOPTS ?= \
  -w -unused-pattern-matching-variable \
  -w -deprecated-ident-entry
COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"
COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) -batch -load-vernac-source
COQCHK="$(COQBIN)coqchk" $(COQINCLUDES)
MENHIR=menhir
CP=cp


# All source files

FILES=src/InsertSort.v

all:
	$(MAKE) depend
	$(MAKE) proof
	$(MAKE) extraction
	$(MAKE) target

proof: $(FILES:.v=.vo)

%.vo: %.v
	@rm -f doc/$(*F).glob
	@echo "$(COQC) $*.v"
	@$(COQC) -dump-glob doc/$(*F).glob $*.v


depend: $(GENERATED) depend1

depend1: $(FILES)
	@echo "Analyzing Coq dependencies"
	@$(COQDEP) $^ > .depend

.depend.extr: extraction/STAMP
	$(MAKE) -f Makefile.extr depend

target: .depend.extr
	$(MAKE) -f Makefile.extr target

clean:
	rm -f $(patsubst %, %/*.vo*, $(DIRS))
	rm -f $(patsubst %, %/.*.aux, $(DIRS))
	rm -rf doc/*.glob
	rm -f .depend
	rm -f extraction/STAMP extraction/*.ml extraction/*.mli
	rm -f *.ml *.mli
	$(MAKE) -f Makefile.extr clean

extraction: extraction/STAMP

extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v
	rm -f extraction/*.ml extraction/*.mli
	$(COQEXEC) extraction/extraction.v
	@if grep 'AXIOM TO BE REALIZED' *.ml; then \
            echo "An error occured during extraction to OCaml code."; \
            exit 2; \
         fi
	touch extraction/STAMP
